The proof relies on two auxiliary results:
completeness (Lemma \ref{l:compl-pase3}) and soundness (Lemma \ref{l:sound-pase3}).
The proof is very similar to the one presented for the case of \evols{2}, and 
considerations concerning the handling of resources (i.e., process \textsc{Control})
are exactly the same. Hence, Remarks \ref{rem:enough} and \ref{rem:wrong} are valid also in this proof.

We first introduce the notion of  encoding of a MM
configuration into \evold{3}. 

\begin{definition}\label{def:confe3}
Let $N$ be a \mm 
with 
registers $r_j ~(j \in \{0,1\})$ and 
instructions $(1:I_1), \ldots, (n:I_n)$.
The encoding of a configuration $(i,m_0, m_1)$ of $N$, denoted
$\encp{(i, m_{0}, m_{1})}{\mmn{3}}$, is defined as:
\[
 \outC{p_i} \parallel e \parallel \encp{r_0 = m_0}{\mmn{3}} \parallel \encp{r_1 = m_1}{\mmn{3}} \parallel \prod^{n}_{i=1} \encp{(i:I_i)}{\mmn{3}} \parallel \reso{\alpha,\beta,\gamma}
\]
where 
\begin{itemize}
\item $\reso{\alpha,\beta,\gamma} \stackrel{\textrm{def}}{=} \prod^{\alpha} \outC{f} \parallel \prod^{\beta} \outC{b} \parallel \prod^{\gamma} \outC{g} \parallel !a.(\outC{f} \parallel \outC{b} \parallel \outC{a}) \parallel !h.(g.\outC{f} \parallel \outC{h})$, with  $\alpha,\beta,\gamma \geq 0$;
\item $\encp{(i:I_i)}{\mmn{3}}, \ldots, \encp{(n:I_n)}{\mmn{3}}$ are as in Table~\ref{t:encod-evold3d};
\item $\encp{r_j = m_j}{\mmn{3}}$ stands for $\componentbbig{r_j}{\prod^{m_j}U_j \parallel Reg_j \parallel \component{c_j}{\gar{\delta}}}$ with 
\begin{itemize}
\item $Reg_j = !inc_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}.u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$ (as in Table~\ref{t:encod-evold3d})
\item $U_j \stackrel{\textrm{def}}{=}  u_j.\update{c_j}{\component{c_j}{\bullet}}.\outC{ack}$
\item $ \garb{\delta}{j} \stackrel{\textrm{def}}{=}  Reg_{j} \parallel \prod^{\delta} U_j $
\end{itemize}
\end{itemize}
\end{definition}

Similarly as before, in addition to the encodings of registers and instructions, 
the encoding of a \mm configuration 
includes a number of resources 
$\outC{f}$ and $\outC{b}$ which are always available during the execution of the machine.
These are represented by process 
$\reso{\alpha,\beta,\gamma}$, which  abstracts the evolution of 
process \textsc{Control} in Table~\ref{t:encod-evold3d}, and the resources
that it produces and maintains (namely, $\alpha$ copies of $\outC{f}$, $\beta$ copies of $\outC{b}$, and $\gamma$ copies of $\outC{g}$).
In addition, 
the encoding of register $j$ in \evold{3} includes a 
``garbage''
process  $ \garb{\delta}{j} $ 
representing residual processes 
which are accumulated during the execution of the encoding; 
as we will see, every interaction with  such a garbage process will result into a deadlocked process.

We prove that given a \mm $N$ there exists a 
computation of process $\encp{N}{\mmn{3}}$ which correctly mimics its behavior. 
We remind that Remark \ref{rem:enough} applies to this case too.

\begin{lemma}\label{lem:correctstep3}
Let $(i, m_0, m_1)$ be a configuration of a \mm $N$. 
\begin{enumerate}
\item If $(i, m_0, m_1)\minskred (i', m_0', m_1')$ then, for some process $P$, 
it holds that $$\encp{(i, m_0, m_1) }{\mmn{3}} \pired^* P \equiv \encp{(i', m_0', m_1') }{\mmn{3}}$$
\item If $(i, m_0, m_1)\notminskred$ then $\encp{(i, m_0, m_1) }{\mmn{3}}\! \Downarrow_{\outC{p_1}}^1$.
\end{enumerate}
\end{lemma}
\begin{proof}
\emph{\underline{Item (1)}:}
We proceed by a case analysis on the instruction  performed by the \mma.
Hence, we distinguish three cases corresponding to the behaviors associated to rules
\textsc{M-Inc}, \textsc{M-Dec}, and \textsc{M-Jmp}.
Without loss of generality, we restrict our analysis to operations on register $r_0$. 

\begin{description}
\item[Case \textsc{M-Inc}:] We have a Minsky configuration $(i, m_0, m_1)$ with 
$(i: \mathtt{INC}(r_0))$. By Definition \ref{def:confe3}, its encoding into \evold{3} is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1) }{\mmn{3}}  & = & 
 \outC{p_i} \parallel e  \parallel
\encp{r_0 = m_0}{\mmn{3}} \parallel \encp{r_1 = m_1}{\mmn{3}} \parallel  \reso{\alpha,\beta,\gamma} \parallel\\
& & !p_i.f.(\outC{g} \parallel b.\outC{inc_0}.ack.\outC{p_{i+1}}) \parallel \prod_{l=1..n,l\neq i} \encp{(l:I_l)}{\mmn{3}} 
\end{eqnarray*}

We then have: $\encp{(i, m_0, m_1) }{\mmn{3}}   \pired R$
where 
$$R = \encp{r_0 = m_0}{\mmn{3}} \parallel f.(\outC{g} \parallel b.\outC{inc_0}.ack.\outC{p_{i+1}}) \parallel \reso{\alpha,\beta,\gamma} \parallel S ,$$
and $S = e \parallel \encp{r_1 = m_1}{\mmn{3}} \parallel \prod_{l=1}^{n} \encp{(l:I_l)}{\mmn{3}}$
stands for the rest of the system.
Starting from $R$, a possible sequence of reductions is the following:
\begin{eqnarray*}
R & \pired & \encp{r_0 = m_0}{\mmn{3}} \parallel b.\outC{inc_0}.ack.\outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S\\
& = &  \componentbig{r_0}{\prod^{m_0}U_0 \parallel !inc_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack}.u_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \\
&&  b.\outC{inc_0}.ack.\outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S\\
& \pired &    \componentbig{r_0}{\prod^{m_0}U_0 \parallel !inc_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack}.u_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \\
&&  \outC{inc_0}.ack.\outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S = R'\\
& \pired  &   \componentbig{r_0}{\prod^{m_0}U_0 \parallel \update{c_0}{\component{c_0}{\bullet}}.\outC{ack}.u_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \\
&&  \parallel ack.\outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S\\
& \pired  &   \componentbig{r_0}{\prod^{m_0}U_0 \parallel \outC{ack}.u_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \\
&&  ack.\outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S \\
& \pired  &   \componentbig{r_0}{\prod^{m_0}U_0 \parallel u_0.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \\
&&  \outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S \\
& = &   \componentbig{r_0}{\prod^{m_0+1}U_0  \parallel Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel  \outC{p_{i+1}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel S = P
\end{eqnarray*}
It is easy to see that $P \equiv \encp{(i+1, m_0+1, m_1)}{\mmn{3}}$, as desired. 
Observe how the number of resources changes: in the first reduction, a copy of $\outC{f}$ is consumed, and  a copy of $\outC{g}$ is released in its place.
Notice that we are assuming that $\beta > 0$, that is, that there is at least one copy of $\outC{b}$.
In fact, since the instruction only takes place after a synchronization on $b$ (i.e., the second reduction above)
the presence of at least one copy of $\outC{b}$ in $\reso{\alpha-1,\beta,\gamma+1}$ is essential to avoid  deadlocks.
For the same reason, it is interesting to observe that 
in $R'$ the computation can only evolve if $\outC{inc_0}$ synchronizes with the replicated input process $inc_0$ inside $r_0$. 
Had it synchronized with the input on $inc_0$ inside $c_0$, the simulation would have reached a deadlock state, 
as there are no other adaptable processes at $c_0$ inside it.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\item[Case \textsc{M-Dec}:] We have a Minsky configuration $(i, m_0, m_1)$ with 
$m_0 > 0$ and 
$(i: \mathtt{DEC}(r_0,s))$. By Definition \ref{def:confe3}, its encoding into \evold{3}  is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1) }{\mmn{3}}  & = & 
 \outC{p_i} \parallel e  \parallel
\encp{r_0 = m_0}{\mmn{3}} \parallel 
\encp{r_1 = m_1}{\mmn{3}}  \parallel \reso{\alpha,\beta,\gamma} \parallel \\
& & !p_i.f.\big(\outC{g} \parallel(\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \\
&& \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s})\big) \parallel  \prod_{l=1..n,l\neq i} \encp{(l:I_l)}{\mmn{3}} 
\end{eqnarray*}

We then have:
\begin{eqnarray*}
\encp{(i, m_0, m_1) }{\mmn{3}} &  \pired &  \encp{r_0 = m_0}{\mmn{3}} \parallel           \reso{\alpha,\beta,\gamma} \parallel \\
& & f.\big(\outC{g} \parallel(\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \\
& & \qquad \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s})\big) \parallel      S = R
\end{eqnarray*}
where $S =  e  \parallel  \encp{r_1 = m_1}{\mmn{3}} \parallel \prod_{l=1}^{n} \encp{(l:I_l)}{\mmn{3}}$ stands for the rest of the system.
Starting from $R$, a possible sequence of reductions is the following:
\begin{eqnarray*} 
R \!\!\!& \pired \!\!\!&  
\encp{r_0 = m_0}{\mmn{3}} \parallel           \reso{\alpha-1,\beta,\gamma+1} \parallel \\
& & \big((\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s})\big) \parallel      S\\
& = \!\!\!&  
\componentbig{r_0}{\prod^{m_0-1}U_0 \parallel u_{0}.\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel 
          \reso{\alpha-1,\beta,\gamma+1}  \\
&& \parallel \big((\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s})\big) \parallel S ~ = R'\\ 
& \pired \!\!\!&  \componentbig{r_0}{\prod^{m_0-1}U_0 \parallel\update{c_0}{\component{c_0}{\bullet}}.\outC{ack} \parallel 
Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel \\
&& ack.(\outC{b} \parallel \outC{p_{i+1}})\parallel S\\  
& \pired \!\!\!&  \componentbig{r_0}{\prod^{m_0-1}U_0 \parallel \outC{ack} \parallel 
Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel \\
&& ack.(\outC{b} \parallel \outC{p_{i+1}})\parallel S\\  
& \pired \!\!\!&  \componentbig{r_0}{\prod^{m_0-1}U_0   \parallel 
Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel  \outC{b} \parallel \outC{p_{i+1}}\parallel S\\  
& \equiv \!\!\!&  \componentbig{r_0}{\prod^{m_0-1}U_0   \parallel 
Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \reso{\alpha-1,\beta+1,\gamma+1} \parallel   \outC{p_{i+1}}\parallel S =P
\end{eqnarray*}
It is easy to see that $P \equiv \encp{(i+1, m_0-1, m_1)}{\mmn{3}}$, as desired. 
Observe how 
in the last reduction 
the presence of at least  a copy of $\outC{u_{0}}$ in $r_{0}$ is fundamental for releasing both an extra copy of $\outC{b}$
and the trigger for the next instruction. 
Notice also that if $\outC{u_{0}}$ in $R'$ synchronizes with $u_0$ inside adaptable process $c_0$ then,
 as in the case of the increment, the simulation would be deadlocked.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Case \textsc{M-Jmp}:] We have a Minsky configuration $(i, 0, m_1)$ and 
$(i: \mathtt{DEC}(r_0,s))$. By Definition \ref{def:confe3}, 
its encoding into \evold{3} is as follows:

\begin{eqnarray*}
\encp{(i, m_0, m_1) }{\mmn{3}}  & = & 
 \outC{p_i} \parallel e  \parallel
\encp{r_0 = 0}{\mmn{3}} \parallel 
\encp{r_1 = m_1}{\mmn{3}}  \parallel \reso{\alpha,\beta,\gamma} \parallel \\
& & !p_i.f.\big(\outC{g} \parallel(\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \\
&& \qquad \quad \qquad \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s})\big) \parallel  \\
& & \prod_{l=1..n,l\neq i} \encp{(l:I_l)}{\mmn{3}} 
\end{eqnarray*}

We then have:
\begin{eqnarray*}
\encp{(i, m_0, m_1) }{\mmn{3}} &  \pired &  \encp{r_0 = 0}{\mmn{3}} \parallel           \reso{\alpha,\beta,\gamma} \parallel
f.\big(\outC{g} \parallel(\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \\
&&\update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s})\big) \parallel      S = R
\end{eqnarray*}
where $S =  e  \parallel  \encp{r_1 = m_1}{\mmn{3}} \parallel \prod_{l=1}^{n} \encp{(l:I_l)}{\mmn{3}}$ stands for the rest of the system.
Starting from $R$, a possible sequence of reductions is the following:
\begin{eqnarray*} 
R & \pired &  
\encp{r_0 = 0}{\mmn{3}} \parallel           \reso{\alpha-1,\beta,\gamma+1} \parallel \\
& & \big(\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + 
\update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s}\big) \parallel      S\\
& = &  
\componentbbig{r_0}{ Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel 
          \reso{\alpha-1,\beta,\gamma+1} \parallel \\
&& \big(\outC{u_0}.ack.(\outC{b} \parallel \outC{p_{i+1}})  + \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s}\big) \parallel S \\ 
& \pired &  \componentbbig{r_0}{Reg_0 \parallel \garb{\delta}{0}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel  \update{r_0}{\component{r_0}{Reg_0 \parallel
\component{c_0}{\bullet}}}.\outC{p_s} \parallel S\\  
& \pired \equiv&  \componentbbig{r_0}{Reg_0 \parallel \component{c_0}{Reg_0 \parallel \garb{\delta}{0}}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel   \outC{p_s}\parallel S \\
& \simeq &  \componentbbig{r_0}{Reg_0 \parallel \component{c_0}{\garb{\delta}{0}}} \parallel \reso{\alpha-1,\beta,\gamma+1} \parallel   \outC{p_s}\parallel S=P
\end{eqnarray*}
It is easy to see that $P \equiv \encp{(s, 0, m_1)}{\mmn{3}}$, as desired. 
Notice that the first reduction results from a synchronization on $f$. 
The second reduction arises from an update action on $c_{0}$, which removes that ``boundary'' for $\garb{\delta}{0}$.
Finally, the third reduction is an update action on $r_{0}$.
We use $\simeq$ to denote the extension of  structural congruence with the axiom $!\pi.P \parallel !\pi.P = !\pi.P$.
\end{description}

\noindent \emph{\underline{Item (2)}:} If $(i, m_0, m_1)\notminskred$ then $i$ corresponds to the $\mathtt{HALT}$ instruction.
Then, by Definition \ref{def:confe3}, 
its encoding into \evold{3} is as follows:
\begin{eqnarray*}
\encp{(i, m_0, m_1) }{\mmn{3}}  & = & 
 \outC{p_i} \parallel e  \parallel
 \encp{r_0 = m_0}{\mmn{3}} \parallel \encp{r_1 = m_1}{\mmn{3}} \parallel \reso{\alpha,\beta,\gamma} \parallel \\
& & !p_i.\outC{h}.h.\update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel \component{c_0}{\bullet}}}. \\
&& \update{c_1}{\bullet}.\update{r_1}{\component{r_1}{Reg_1 \parallel
\component{c_1}{\bullet}}}.\outC{p_1} \parallel \prod_{l=1..n,l\neq i} \encp{(l:I_l)}{\mmn{3}} 
\end{eqnarray*}

We then have: $\encp{(i, m_0, m_1) }{\mmn{3}}   \pired  R$ where
\begin{eqnarray*}
 R &=&
 \encp{r_0 = m_0}{\mmn{3}}  \parallel \encp{r_1 = m_1}{\mmn{3}} \parallel \reso{\alpha,\beta,\gamma} \parallel\\
 && \outC{h}.h.\update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel \component{c_0}{\bullet}}}. \update{c_1}{\bullet}.\update{r_1}{\component{r_1}{Reg_1 \parallel \component{c_1}{\bullet}}}.\outC{p_1}  \parallel S
\end{eqnarray*}
where $S =  e  \parallel  \prod_{l=1}^{n}\encp{(l:I_l)}{\mmn{3}}$ stands for the rest of the system.
Starting from $R$, a possible sequence of reductions is the following:
\begin{eqnarray*} 
R & \pired^{*} &   \encp{r_0 = m_0}{\mmn{3}}  \parallel \encp{r_1 = m_1}{\mmn{3}} \parallel \reso{\alpha+c,\beta,\gamma-c} \parallel S \parallel\\
 && \update{c_0}{\bullet}.\update{r_0}{\component{r_0}{Reg_0 \parallel \component{c_0}{\bullet}}}. \update{c_1}{\bullet}.\update{r_1}{\component{r_1}{Reg_1 \parallel \component{c_1}{\bullet}}}.\outC{p_1} =R_1
\end{eqnarray*}
where the output on $h$ in $R$ interacted with  process $\reso{\alpha,\beta,\gamma}$
so as to replace $c$ outputs on $g$ with $c$ outputs on $f$.
After that,  a synchronization on $h$ took place between 
the evolutions of $\reso{\alpha,\beta,\gamma}$ and of $R$.
We now have:
 \begin{eqnarray*} 
R_1 \!\!\!& \pired\!\!\! &  \componentbig{r_0}{\prod^{m_0}U_0 \parallel Reg_0 \parallel \garb{\delta_0}{0}}  \parallel \componentbig{r_1}{\prod^{m_1}U_1 \parallel Reg_1 \parallel \component{c_1}{\garb{\delta_1}{1}}} \parallel S  \parallel\\
 && \update{r_0}{\componentbbig{r_0}{Reg_0 \parallel \component{c_0}{\bullet}}}. \update{c_1}{\bullet}.\update{r_1}{\componentbbig{r_1}{Reg_1 \parallel \component{c_1}{\bullet}}}.\outC{p_1} \parallel \reso{\alpha+c,\beta,\gamma-c}\\
& \pired  \simeq \!\!\!& \componentbig{r_0}{Reg_0 \parallel \component{c_0}{\garb{\delta_0+m_0}{0}}}  \parallel \componentbig{r_1}{\prod^{m_1}U_1 \parallel Reg_1 \parallel \component{c_1}{\garb{\delta_1}{1}}} \parallel S  \parallel\\
 && \update{c_1}{\bullet}.\update{r_1}{\componentbbig{r_1}{Reg_1 \parallel \component{c_1}{\bullet}}}.\outC{p_1} \parallel \reso{\alpha+c,\beta,\gamma-c}\\
& \pired \!\!\! & \component{r_0}{Reg_0 \parallel \component{c_0}{\gar{\delta_0+m_0}}}  \parallel \component{r_1}{\prod^{m_1}U_1 \parallel Reg_1 \parallel \garb{\delta_1}{1}} \parallel S  \parallel\\
 && \update{r_1}{\componentbbig{r_1}{Reg_1 \parallel \component{c_1}{\bullet}}}.\outC{p_1} \parallel \reso{\alpha+c,\beta,\gamma-c}\\
& \pired  \simeq \!\!\!& \componentbig{r_0}{Reg_0 \parallel \component{c_0}{\garb{\delta_0+m_0}{0}}}  \parallel \componentbig{r_1}{Reg_1 \parallel \component{c_1}{\garb{\delta_1+m_1}{1}}} \parallel S \parallel\\
&&  \outC{p_1} \parallel \reso{\alpha+c,\beta,\gamma-c}  
\end{eqnarray*}
which is easily seen to correspond to $\encp{(1, 0, 0) }{\mmn{3}}$, and thus $\encp{(i, m_0, m_1) }{\mmn{3}}\! \Downarrow_{\outC{p_1}}^1$.
\end{proof}


It is straightforward to see that Remark \ref{rem:wrong} is valid for $\encp{N}{\mmn{3}}$ too.
Unsurprisingly, the proof concludes following the same lines of the proof of Lemma \ref{th:corrE2}.


\begin{lemma}[Completeness]\label{l:compl-pase3}
Let $N$ be a \mm. If $N$ terminates then $\encp{N}{\mmn{3}} \barbw{e}$.
\end{lemma}
\begin{proof}
Recall that $N$ is said to terminate if there exists a computation 
$$(1,0,0) \minskred ^* (h, 0, 0)$$
such that $(h: \mathtt{HALT})$.
Lemma \ref{lem:correctstep3} ensures the existence of a process $P$ such that 
$\encp{(1, 0, 0)}{\mmn{3}} \pired ^* P \equiv \encp{(h, 0, 0)}{\mmn{3}}$, with 
$P \Downarrow_{\outC{p_{1}}}^1$.
This  ensures that every time that the encoding of $N$ reaches $\mathtt{HALT}$ the simulation is restarted.
Therefore,  termination of $N$ ensures that $\encp{N}{\mmn{3}}$
has an infinite computation:
since the encoding always 
exhibits barb $e$, we can conclude that $\encp{N}{\mmn{3}} \barbw{e}$.
\end{proof}




\begin{lemma}[Soundness]\label{l:sound-pase3} 
Let $N$ be a \mm. If $N$ does not terminate then $\encp{N}{\mmn{3}} \negbarbw{e}$.
\end{lemma}
\begin{proof}
It is enough to prove that if $N$ does not terminate 
(that is, if $N$ does not reach a  $\mathtt{HALT}$ instruction)
then all the computations of $\encp{N}{\mmn{3}}$ are finite.
Since the encoding can mimic the behavior of $N$ both correctly and incorrectly, we have two possible cases:
\begin{enumerate}
 \item
 In the first case, 
  the simulation of $\encp{N}{\mmn{3}}$ is correct and no erroneous steps are introduced.
Notice that at every instruction an output on $f$ is consumed permanently: these
copies of $\outC{f}$ are only recreated when invoking a $\mathtt{HALT}$ instruction, which converts every $\outC{g}$ into a $\outC{f}$.
Since a $\mathtt{HALT}$ instruction is never reached, 
new copies  of $\outC{f}$ are never recreated, and 
the computation of process $\encp{N}{\mmn{3}}$ has necessarily to be  finite.

 \item 
 In the second case, 
 the simulation is not correct and one or more wrong guesses occurred
 in the simulation of a decrement-and-jump instruction.
 Here, in addition to the possibility of deadlocks described in Item (1) above, 
 erroneous computations constitute another source of deadlocks.
 In fact, as detailed in Remark \ref{rem:wrong}, 
 for each one of such wrong guesses a copy of $\outC{b}$ is permanently lost. 
 Finally, the last source of error is represented by a wrong synchronization with $inc_j$ (in case of an increment) or $u_j$ (in case of a decrement) inside the adaptable process $c_j$. As 
 described above, those wrong synchronizations lead to a deadlock. 
An arbitrary number of wrong guesses may thus lead to a state in which there are no outputs on $b$.
As discussed at the end of the case of the \textsc{M-Inc} in the proof of Lemma \ref{lem:correctstep3}, 
the encoding of an increment instruction
reaches a deadlock if a copy of $\outC{b}$ is not available.
This means that wrong guesses in simulating a decrement-and-jump instruction may induce deadlocks when simulating an increment instruction.

\end{enumerate}


Hence, as all the computations of $\encp{N}{\mmn{3}}$ are finite, therefore $\encp{N}{\mmn{3}}$  barb $e$
cannot be exposed an infinite number of times.
\end{proof}

We are now ready to repeat the statement of Lemma \ref{th:corrE3}, in page \pageref{th:corrE3}:

\begin{lemma}[\ref{th:corrE3}]
Let $N$ be a \mm. $N$ terminates iff $\encp{N}{\mmn{3}} \barbw{e}$.
\end{lemma}

\begin{proof}
It follows directly from Lemmas \ref{l:compl-pase3} and \ref{l:sound-pase3}.
\end{proof}